Brief introduction about why we need system verification and what is Process Analysis Toolkit and information related to PAT issues. And also give an outline about how this manual is organized.

• 1.1 Preface
• 1.2 Organization

This chapter will give you the detailed and helpful information about how to install, configure and use PAT.

• 2.1 Installation
• 2.2 Graphic User Interface
• 2.3 System Configuration
• 2.4 LTL to Automata Converter
• 2.5 Using C# Library
• 2.6 Keyboard Shortcuts
• 2.7 Command Line
• 
  

This chapter helps you with the detailed information about how to play with PAT, including the depth knowledge about PAT's architecture and different modules. Each module has a specific language reference and a tutorial part which shows how PAT can be used in different domains such as reasoning about strict Real Time System problems.

• 3.1 Communication Sequence Process Module
• 3.2 Real Time System Module
• 3.3 Probability CSP Module
• 3.4 Probability RTS Module
• 3.5 Labeled Transition System (LTS) Module
• 3.6 Timed Automata (TA) Module 
• 3.7 NesC Module
• 3.8 Orc Module
• 3.9 Stateflow (MDL) Module
• 3.10 Secutiry Module
• 3.11 Web Service Module
• 3.12 Import UML into PAT
• 
  

• 4.1 Fairness
• 4.2 Parallel Verification
• 4.3 Verification of Infinite Systems
• 4.4 Verification of Linearizability
• 4.5 Timed Zenoness Checking
• 
  

Questions and answers about installing and using PAT.

• Installation FAQ
• Using PAT FAQ
• 
  

Give a list of publications and books this manual referenced.